/* Copyright (c) 2011-2012 ISP RAS, Moscow. For more information please write to

      mermakov@ispras.ru
      svartanov@ispras.ru

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*/

package ru.ispras.coffeemachine.trace;

import java.io.BufferedReader;
import java.io.StringReader;
import java.text.ParseException;
import java.util.ArrayList;
import java.util.List;

import ru.ispras.coffeemachine.util.Logger;
import ru.ispras.coffeemachine.util.Options;

/**
 * STP answer parsing
 *
 * @author Sergey Vartanov <me@enzet.ru>
 * @version 1.2.0
 * @since 2011-10-04
 */
public class Glace
{
	/**
	 * STP trace
	 */
	private final String trace;
	private final int[] values;
	public List<byte[]> files;

	public Glace(String trace, int maxVariableNumber)
	{
		this.trace = trace;
		values = new int[maxVariableNumber];

		for (int i = 0; i < maxVariableNumber; i++)
		{
			values[i] = -1;
		}

		files = new ArrayList<byte[]>();
		for (int i = 0; i < Options.inputs.size(); i++)
		{
			files.add(new byte[Options.inputLengths.get(i)]);
		}
	}

	/**
	 * STP trace parsing for new input files
	 */
	public boolean parse() throws Exception
	{
		Logger.debug(trace);

		boolean valid = false;

		BufferedReader in = new BufferedReader(new StringReader(trace));
		String line;
		while ((line = in.readLine()) != null)
		{
			line = line.trim();

			if (line.equals("Invalid.")) break;

			if (line.equals("Valid."))
			{
				Logger.verbose("Oops. STP cannot find input.");
				System.out.print("?");
				valid = true;
				break;
			}

			if (line.length() < 8) { throw new ParseException(line, 0); }

			if (!line.substring(0, 6).equals("ASSERT"))
			{
				// Logger.error("irregular assert on \"" + line + "\"");
				// Logger.log("\nFull STP answer:\n" + trace);

				// CoffeeMachine.close();

				throw new ParseException(line, 0);
			}
			else
			{
				line = line.substring(8);

				if (line.charAt(0) == 'x')
				{
					line = line.substring(4);

					int number = 0;
					try {
						number = Integer.parseInt(line.substring(0, line.indexOf(' '))) - 1;
					} catch (NumberFormatException e) {
						continue;
					}
					line = line.substring(line.indexOf(' ') + 3);

					int radix = 0;

					if (line.charAt(1) == 'x') radix = 16;
					else if (line.charAt(1) == 'b') radix = 2;
					else
					{
						throw new Exception("unknown radix");
					}

					long value;

					try
					{
						value = Long.parseLong(line.substring(2, line.indexOf(' ')).toLowerCase(), radix);

						values[number] = (int) value;
					}
					catch (NumberFormatException e)
					{
						Logger.error("cannot parse " + line.substring(2, line.indexOf(' ')) + " with radix " + radix);
						e.printStackTrace();
						System.exit(0);
					}
				}
				else throw new Exception("unknown variable type");
			}
		}

		/**
		 * FIXME Next operations for all specified input files
		 */
		for (int i = 0; i < Options.inputLengths.get(0); i++)
		{
			files.get(0)[i] = (byte) values[i];
		}

		return valid;
	}

	// Getter

	public int getValue(int number)
	{
		return values[number];
	}

	public String getFileContent(int fileNumber)
	{
		return new String(files.get(fileNumber));
	}
}
